$\forall$${\it es}$:ES, $T$:Type. strong{-}subtype($T$;E) $\Rightarrow$ ($\forall$$f$:($T$$\rightarrow$$T$). ($\forall$$x$:$T$. $f$($x$) c$\leq$ $x$) $\Rightarrow$ retraction($T$;$f$))